Type of mathematical object
In set theory, Silver machines are devices used for bypassing the use of fine structure in proofs of statements holding in L. They were invented by set theorist Jack Silver as a means of proving global square holds in the constructible universe.
An ordinal
is *definable from a class of ordinals X if and only if there is a formula
and ordinals
such that
is the unique ordinal for which
where for all
we define
to be the name for
within
.
A structure
is eligible if and only if:
.
- < is the ordering on On restricted to X.
is a partial function from
to X, for some integer k(i).
If
is an eligible structure then
is defined to be as before but with all occurrences of X replaced with
.
Let
be two eligible structures which have the same function k. Then we say
if
and
we have:
A Silver machine is an eligible structure of the form
which satisfies the following conditions:
Condensation principle. If
then there is an
such that
.
Finiteness principle. For each
there is a finite set
such that for any set
we have
![{\displaystyle M_{\lambda +1}[A]\subseteq M_{\lambda }[(A\cap \lambda )\cup H]\cup \{\lambda \}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5fe79b9239ce264588e6812edb801bddd8f79185)
Skolem property. If
is *definable from the set
, then
; moreover there is an ordinal
, uniformly
definable from
, such that
.